f3(true, x, y) -> f3(gt2(x, y), s1(x), s1(s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
f3(true, x, y) -> f3(gt2(x, y), s1(x), s1(s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
F3(true, x, y) -> F3(gt2(x, y), s1(x), s1(s1(y)))
F3(true, x, y) -> GT2(x, y)
GT2(s1(u), s1(v)) -> GT2(u, v)
f3(true, x, y) -> f3(gt2(x, y), s1(x), s1(s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F3(true, x, y) -> F3(gt2(x, y), s1(x), s1(s1(y)))
F3(true, x, y) -> GT2(x, y)
GT2(s1(u), s1(v)) -> GT2(u, v)
f3(true, x, y) -> f3(gt2(x, y), s1(x), s1(s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
GT2(s1(u), s1(v)) -> GT2(u, v)
f3(true, x, y) -> f3(gt2(x, y), s1(x), s1(s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
GT2(s1(u), s1(v)) -> GT2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
gt2(0, x0)
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
GT2(s1(u), s1(v)) -> GT2(u, v)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
F3(true, x, y) -> F3(gt2(x, y), s1(x), s1(s1(y)))
f3(true, x, y) -> f3(gt2(x, y), s1(x), s1(s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ UsableRulesProof
F3(true, x, y) -> F3(gt2(x, y), s1(x), s1(s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
f3(true, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ UsableRulesProof
F3(true, x, y) -> F3(gt2(x, y), s1(x), s1(s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)
F3(true, 0, x0) -> F3(false, s1(0), s1(s1(x0)))
F3(true, s1(x0), s1(x1)) -> F3(gt2(x0, x1), s1(s1(x0)), s1(s1(s1(x1))))
F3(true, s1(x0), 0) -> F3(true, s1(s1(x0)), s1(s1(0)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ UsableRulesProof
F3(true, 0, x0) -> F3(false, s1(0), s1(s1(x0)))
F3(true, s1(x0), 0) -> F3(true, s1(s1(x0)), s1(s1(0)))
F3(true, s1(x0), s1(x1)) -> F3(gt2(x0, x1), s1(s1(x0)), s1(s1(s1(x1))))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ UsableRulesProof
F3(true, s1(x0), s1(x1)) -> F3(gt2(x0, x1), s1(s1(x0)), s1(s1(s1(x1))))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)
F3(true, s1(s1(z0)), s1(s1(s1(z1)))) -> F3(gt2(s1(z0), s1(s1(z1))), s1(s1(s1(z0))), s1(s1(s1(s1(s1(z1))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ UsableRulesProof
F3(true, s1(s1(z0)), s1(s1(s1(z1)))) -> F3(gt2(s1(z0), s1(s1(z1))), s1(s1(s1(z0))), s1(s1(s1(s1(s1(z1))))))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)
F3(true, s1(s1(z0)), s1(s1(s1(z1)))) -> F3(gt2(z0, s1(z1)), s1(s1(s1(z0))), s1(s1(s1(s1(s1(z1))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
F3(true, s1(s1(z0)), s1(s1(s1(z1)))) -> F3(gt2(z0, s1(z1)), s1(s1(s1(z0))), s1(s1(s1(s1(s1(z1))))))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
F3(true, x, y) -> F3(gt2(x, y), s1(x), s1(s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
f3(true, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
F3(true, x, y) -> F3(gt2(x, y), s1(x), s1(s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
gt2(0, x0)
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)